(TML)

"X:*";;
"Y:*";;
"H:*->*";;
"F:*->(*->*)";;
"G:*->(*->*)";;
"PHI:*->*";;
"PSI:*->*";;


let funPHI = "(\PHI X. F X (PHI (H X)))";;
let funPSI = "(\PSI X. G X (PSI (H X)))";;
let funTET = "(\TET X. F X (G (H X) (TET (H (H X)))))";;


let th1 = ASSUME "PHI == FIX ↑funPHI";;
let th2 = ASSUME "PSI == FIX ↑funPSI";;
let th3 = ASSUME "TET == FIX ↑funTET";;




let ss1 = BASICSS;;

let goal1 = "!X. PHI X == F X (G (H X) (PHI (H (H X))))",
            ss1,[]:form list;;

let eqPHIPSI = ASSUME "PHI == PSI";;

let TAC1 = UNWINDOCCSTAC[1] th1 THEN SIMPTAC
           THEN SUBSOCCSTAC[([1],eqPHIPSI)] THEN
           UNWINDTAC th2 THEN SIMPTAC THEN
           SUBSTAC[eqPHIPSI] THEN SIMPTAC;;



let th4 = ASSUME "PHI == FIX(\PHI' X.F X(G (H X)(PHI'(H(H X)))))";;


let goal3 = "PHI == FIX(\PHI' X. F X(G (H X)(PHI'(H(H X)))))",
            ss1,[]:form list;;


let goal2 = "FIX(\PHI' X. F X(G(H X)(PHI'(H(H X))))) << PHI"
            ,ss1,[]:form list;;


let goal4 = "TET << PHI",ss1,[]:form list;;

let TAC4 = WEAKFIXTAC th3 THEN SIMPTAC THEN APPLYTAC2
           THEN SIMPTAC THEN UNWINDOCCSTAC[2] th1 THEN SIMPTAC
           THEN SUBSTAC [eqPHIPSI] THEN UNWINDOCCSTAC[2] th2
           THEN SIMPTAC;;


let th33 = ASSUME "TET3 == FIX(\TET3. (↑funPHI (↑funPSI TET3)))";;

let goal33 = "TET == TET3",ss1,[]:form list;;

let TAC33 = INDUCTAC[th3;th33] THEN SIMPTAC THEN GREUTAC THEN SIMPTAC;;